\subsection{Variants of the Correctness Properties}
%\todo{We could discuss variants of the considered properties (eg. non consecutive barbs or different mechanisms to construct the parametrically defined initial configurations).}

In this presentation, we have studied correctness of adaptable processes from a rather general perspective; 
in fact, the definition of \OG and \LG are based only on minimal observations on the behavior of the system.
This allows us to reason about the interplay between correctness and adaptation for diverse classes of concurrent systems.
More informative properties (relating correctness and the structure of the system, for instance)
can be devised according to the nature of some particular setting.
%we have opted for \OG and \LG with the objective of 

In this context, it is worth noticing that the technical machinery required for 
our (un)decidability results can be adapted to handle a slightly different definition of the adaptation problems stated
%Results similar to the ones discussed here can be obtained even if we slightly modify the problems in 
in Definition \ref{def:adaptprob}.
More precisely, 
such problems can be relaxed so as to consider \emph{non consecutive} error occurrences, rather than consecutive ones.
For this purpose, 
we modify the notion of barbs (cf. Definition \ref{d:barb}) 
by admitting an arbitrary number of reductions between the actual error barbs:
%in such a way that instead of considering consecutive barbs, we admit that they can be  followed by an arbitrary number of reductions:
\begin{definition}[Barbs - Alternative Definition]\label{d:barb2}
Let $P$ be an $\mathcal{E}$ process, and let $\alpha$ be an action in $\{a, \outC{a} \mid a \in \mathcal{N}  \}$.
\begin{itemize}
\item Given  $k > 0$, we write $P\barb{\alpha}^{k}$ 
%if there exists a computation 
iff there exist $Q_{1},\ldots, Q_{k}$ such that
$P \pired^{*} Q_1 \pired^{*} \ldots \pired^{*} Q_k$
with $Q_i \downarrow_\alpha$, for every $i \in \{1,\ldots, k\}$.
\item We write $P\barb{\alpha}^{\omega}$ iff
there exists an infinite computation
$P \pired^* Q_1 \pired^{*} Q_2 \pired^{*}  \ldots$
with $Q_i \downarrow_\alpha$ for every $i \in \mathbb{N}$.
\end{itemize}
Furthermore, we  use $\negbarbk{\alpha}$ and $\negbarbw{\alpha}$ to denote the negation of $\barbk{\alpha}$ and $\barbw{\alpha}$, with the expected meaning.
\end{definition}

Variants of 
\LG and \OG can be then restated considering the new definition above. 
Thus, given a set of clusters $\BC_P^M$ and a
barb $e$ then   the \OG problems consists in checking whether all computations of processes in $\BC_P^M$ have at most $k$  states exhibiting $e$.
Similarly, \LG consists in checking whether there is
no computation in which $e$
is observable in infinitely many distinct states.
Given these alternative definitions of \LG and \OG, (un)decidability results can be easily derived from the ones presented here. 
In fact, Table \ref{t:results} remains unchanged under the alternative adaptation problems. 
More precisely, straightforwardly all undecidability results hold.
For the decidability results, we should adapt the WSTS construction and the Petri net simulation.
In particular, to show decidability of the alternative definition of \OG  for \evold{2} processes, 
it is enough to slightly change the definition of $\mathsf{fb}_{\alpha}(S)$ (Definition \ref{def:fbk}) and substituting the occurrences of $pb_S$ with $\Pred_S^*$ whose effectiveness is guaranteed by Theorem \ref{th:fb}.
Concerning the decidability of \LG for \evols{3}, the Petri net semantics presented in Section \ref{sec:evol3}
reduces this alternative version of the property to the \emph{repeated coverability} problem. This problem
is known to be decidable for Petri nets, see e.g. \cite{E03}.


%\todo{Gigio: can we add something for the Petri net? C'era altro da dire?}

%We can therefore obtained the same results, summed up in the following table.
%
%\begin{tabular}{c|c|c}
%		& Dynamic Topology & Static Topology \\
%\hline \hline
%\evol{1}	&~ \OG undec ~/~\LG undec ~& ~\OG undec~/~\LG undec~\\
%\hline
%\evol{2}	& ~ \OG dec~/~\LG undec ~ & ~ \OG dec~/~\LG undec \\
%\hline
%\evol{3}	& ~ \OG dec~/~\LG undec ~ & \OG~dec~/~\LG dec 
%\end{tabular} 

